Nuprl Lemma : ma-trivial-interface_wf 11,40
i:Id, k:{k:Knd| hasloc(k;i)} , V, T:Type, f:(V(T + Top)).
ma-trivial-interface(i;k;V;f)  MaInterface(T) 
latex

Definitionsma-trivial-interface(i;k;V;f), MaInterface(T), t  T, Top, left + right, x:AB(x), x:A. B(x), Type, Knd, b, {x:A| B(x)} , Id, Atom$n, State(ds), x:A  B(x), x. t(x), a:A fp B(a), x.A(x)
Lemmasfpf-single wf, fpf wf, decl-state wf, top wf

origin